es:ES, e:E. es-init(es;e)  e   True 

latex

Definitions	t  T, P  Q, x:A. B(x), e  e' , es-init(es;e), Trans x,y:T. E(x;y), True, P  Q, Prop, (e <loc e'), E, P  Q, P & Q, P  Q, 1of(t), b, A, b, , first(e), Unit, ES, {T}, x. t(x), WellFnd{i}(A;x,y.R(x;y)), pred(e)
Lemmas	es-locl-wellfnd, es-locl wf, iff wf, es-E wf, event system wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, es-first wf, bool wf, bnot wf, not wf, assert wf, es-le-self, es-pred-locl, es-le wf, true wf, es-le-trans, es-init wf, es-pred wf, es-pred-le